'''
Created on 28/09/2009

@author: b1u3fox
'''
import interprete

from logica.proposiciones import *
from logica.esquema import *

class Token(interprete.Token):
    
    ABS = 'Abs'             
    ADJ = 'Adj'
    ASOC = 'Asoc'
    ATAUT = 'ATaut'
    CADENA = 'Cadena' #.* (str)
    COMA = ','
    CONM = 'Conm'
    CONTR = 'Contr'
    DCOND = 'DC'
    DIMPL = 'DblImpl'
    DEM = 'Dem'
    IMPL = 'Impl'
    DIST = 'Dist'
    DBLNEG = 'DblNeg'
    ID = 'Identificador'         #[a-zA-Z]+
    IDEMP = 'Idemp'
    IGUAL = '='
    LDM = 'DeMorgan'
    MP = 'MP'
    MT = 'MT'
    MTP = 'MTP'
    NO = '~'
    NUMERO = 'Numero'       #[0-9]+
    O = '|'
    PABRE = '('
    PCIERRA = ')'
    PDEM = 'PorDemostrar'
    PUNTO = '.'
    RAA = 'RAA'
    RP = 'RP'
    SD = 'SD'
    SH = 'SH'
    SI = '->'
    SII = '<->'
    SIMPL = 'Simpl'
    TAUT = 'Taut'
    Y = '&'
    
    PALABRAS_RESERVADAS = [ABS, ADJ, ASOC, ATAUT, CONM, CONTR, DCOND, DIMPL, 
                           DEM, IMPL, DIST, DBLNEG, IDEMP, LDM, MP, MT, MTP, 
                           PDEM, RAA, RP, SD, SH, SIMPL, TAUT]
    

class Analex(interprete.Analex):
    
    def _analizar(self):
        caracter_actual = self.multilinea.caracter_actual()
        while caracter_actual.isspace() and not self.multilinea.fda:
            if caracter_actual == '\n':
                self.nro_linea += 1
                self.nro_caracter = 1
            self.multilinea.avanzar()
            self.nro_caracter += 1
            caracter_actual = self.multilinea.caracter_actual()
        inicio = self.multilinea.indice_caracter
        token = None
        self.acumulador = ''
        if self.multilinea.fda:
            token = Token(Token.FDA, None)
            self.multilinea.avanzar()
            self.nro_caracter += 1
        elif caracter_actual == ',':
            token = Token(Token.COMA, None)
            self.multilinea.avanzar()
            self.nro_caracter += 1
        elif caracter_actual == '=':
            token = Token(Token.IGUAL, None)
            self.multilinea.avanzar()
            self.nro_caracter += 1
        elif caracter_actual == Token.NO:
            token = Token(Token.NO, None)
            self.multilinea.avanzar()
            self.nro_caracter += 1
        elif caracter_actual == Token.O:
            token = Token(Token.O, None)
            self.multilinea.avanzar()
            self.nro_caracter += 1
        elif caracter_actual == '(':
            token = Token(Token.PABRE, None)
            self.multilinea.avanzar()
            self.nro_caracter += 1
        elif caracter_actual == ')':
            token = Token(Token.PCIERRA, None)
            self.multilinea.avanzar()
            self.nro_caracter += 1
        elif caracter_actual == '.':
            token = Token(Token.PUNTO, None)
            self.multilinea.avanzar()
            self.nro_caracter += 1
        elif caracter_actual == Token.Y:
            token = Token(Token.Y, None)
            self.multilinea.avanzar()
            self.nro_caracter += 1
        elif caracter_actual == '-':
            self.multilinea.avanzar()
            self.nro_caracter += 1
            caracter_actual = self.multilinea.caracter_actual()
            if caracter_actual == '>':
                token = Token(Token.SI, None)
                self.multilinea.avanzar()
                self.nro_caracter += 1
        elif caracter_actual == '<':
            self.multilinea.avanzar()
            self.nro_caracter += 1
            caracter_actual = self.multilinea.caracter_actual()
            if caracter_actual == '-':
                self.multilinea.avanzar()
                self.nro_caracter += 1
                caracter_actual = self.multilinea.caracter_actual()
                if caracter_actual == '>':
                    token = Token(Token.SII, None)
                    self.multilinea.avanzar()
                    self.nro_caracter += 1
        elif caracter_actual == '"':
            self.multilinea.avanzar()
            self.nro_caracter += 1
            caracter_actual = self.multilinea.caracter_actual()
            while not caracter_actual == '"' and not self.multilinea.fda:
                self.acumulador += caracter_actual
                self.multilinea.avanzar()
                self.nro_caracter += 1
                caracter_actual = self.multilinea.caracter_actual()
            if not self.multilinea.fda:
                token = Token(Token.CADENA, self.acumulador)
                self.multilinea.avanzar()
                self.nro_caracter += 1
        elif caracter_actual.isalpha():
            while caracter_actual.isalnum() and not self.multilinea.fda:
                self.acumulador += caracter_actual
                self.multilinea.avanzar()
                self.nro_caracter += 1
                caracter_actual = self.multilinea.caracter_actual()
            if self.acumulador in Token.PALABRAS_RESERVADAS:
                token = Token(self.acumulador, None)
            else:
                nombre = self.acumulador
                simbolo = self.tabla_simbolos.obtener_simbolo(nombre)
                token = Token(Token.ID, simbolo)
        elif caracter_actual.isdigit():
            while caracter_actual.isdigit() and not self.multilinea.fda:
                self.acumulador += caracter_actual
                self.multilinea.avanzar()
                self.nro_caracter += 1
                caracter_actual = self.multilinea.caracter_actual()
            token = Token(Token.NUMERO, int(self.acumulador))
        if not token:
            token = Token(Token.ERROR, None)
            self.multilinea.avanzar()
            self.nro_caracter += 1
        token.inicio = inicio
        token.fin = self.multilinea.indice_caracter
        if self.multilinea.fda:
            token.fin += 1
        return token


class Parser(interprete.Parser):
    # Conjuntos First para el Parser predictivo.
    F = {}
    F['pMasNumero'] = set([Token.COMA]) # U {}
    F['pParametros'] = set([Token.PABRE]) # U {}
    F['pEquivalenciaLogica'] = set([Token.IDEMP, Token.CONM, Token.ASOC, 
                                    Token.DIST, Token.IMPL, Token.DIMPL, 
                                    Token.LDM, Token.TAUT, Token.ATAUT, 
                                    Token.ABS, Token.DBLNEG])
    F['pReglaInferencia'] = set([Token.MP, Token.MT, Token.SIMPL, Token.ADJ, 
                                 Token.SH, Token.SD, Token.RP, Token.DEM, 
                                 Token.PDEM, Token.DCOND, Token.RAA, 
                                 Token.CONTR]).union(F['pEquivalenciaLogica'])
    F['pJustificacion'] = F['pReglaInferencia']
    F['pConectivo'] = set([Token.O, Token.Y, Token.SI, Token.SII])
    F['pConProp'] = F['pConectivo'] # U {}
    F['pEnunciado'] = set([Token.ID])
    F['pNegacion'] = set([Token.NO])
    F['pPropInterna'] = set([Token.PABRE]).union(F['pEnunciado'], 
                                                 F['pNegacion'])
    F['pProposicion'] = F['pPropInterna']
    F['pNumeral'] = set([Token.NUMERO])
    F['pArgumento'] = F['pNumeral']
    F['pDeclaracion'] = F['pEnunciado']
    F['pSentencia'] = set().union(F['pDeclaracion'], F['pArgumento'])
    F['pMasSentencia'] = F['pSentencia']
    F['pEsquema'] = F['pSentencia']
    
    def __init__(self, tabla_simbolos=None):
        interprete.Parser.__init__(self, tabla_simbolos)
        self.analex = Analex(self.tabla_simbolos)
        self.esquema = None
        self.argumentos = {}
        self.elementos = {}
        self.numeral = None
        self.proposicion = None
        self.propinterna = None
        self.enunciado = None
        self.conprop = None
        self.conectivo = None
        self.regla_inferencia = None
        self.equivalencia_logica = None
        self.parametros = []
    
    def parse(self, cadena):
        self.analex.iniciar(cadena)
        self.error_found = False
        self.__p_esquema()

    def __p_esquema(self):
        "Esquema := Sentencia MasSentencia"
        self.esquema = None
        self.argumentos = {}
        self.elementos = {}
        token = self.analex.preanalisis()
        if token.tipo in self.F['pSentencia']:
            self.__p_sentencia()
            self.__p_massentencia()
            self.esquema = EsquemaInferencia(self.argumentos, self.elementos)
        else:
            self.error_found = True
            self._arrojar_error(self.F['pSentencia'])
            
    def __p_sentencia(self):
        "Sentencia := Declaracion | Argumento"
        token = self.analex.preanalisis()
        if token.tipo in self.F['pDeclaracion']:
            self.__p_declaracion()
        elif token.tipo in self.F['pArgumento']:
            self.__p_argumento()
        else:
            self.error_found = True
            self._arrojar_error(self.F['pSentencia'])
            
    def __p_declaracion(self):
        "Declaracion := Enunciado IGUAL CADENA"
        self.__p_enunciado()
        token = self.analex.preanalisis()
        self._emparejar(token, Token.IGUAL)
        token = self.analex.preanalisis()
        self._emparejar(token, Token.CADENA)
        descripcion = token.valor
        enunciado = self.enunciado
        enunciado.descripcion = descripcion
    
    def __p_argumento(self):
        "Argumento := Numeral Proposicion Justificacion"
        self.__p_numeral()
        self.__p_proposicion()
        self.__p_justificacion()
        argumento = Argumento(self.numeral, self.proposicion, 
                              self.justificacion)
        self.argumentos[self.numeral] = argumento
    
    def __p_numeral(self):
        "Numeral := NUMERO PUNTO"
        self.numeral = None
        token = self.analex.preanalisis()
        self._emparejar(token, Token.NUMERO)
        self.numeral = str(token.valor)
        token = self.analex.preanalisis()
        self._emparejar(token, Token.PUNTO)
    
    def __p_proposicion(self):
        "Proposicion := PropInterna ConProp"
        self.proposicion = None
        self.__p_propinterna()
        self.__p_conprop()
        self.proposicion = self.conprop or self.propinterna
    
    def __p_propinterna(self):
        "PropInterna := Enunciado | Negacion | PABRE Proposicion PCIERRA"
        self.propinterna = None
        token = self.analex.preanalisis()
        if token.tipo in self.F['pEnunciado']:
            self.__p_enunciado()
            self.propinterna = self.enunciado
        elif token.tipo in self.F['pNegacion']:
            self.__p_negacion()
            self.propinterna = self.negacion
        elif token.tipo == Token.PABRE:
            self._emparejar(token, Token.PABRE)
            self.__p_proposicion()
            token = self.analex.preanalisis()
            self._emparejar(token, Token.PCIERRA)
            self.propinterna = self.proposicion
        else:
            self._arrojar_error(self.F['pPropInterna'])
            
    def __p_negacion(self):
        "Negacion := NO PropInterna"
        self.negacion = None
        token = self.analex.preanalisis()
        self._emparejar(token, Token.NO)
        self.__p_propinterna()
        self.negacion = Negacion(self.propinterna)
    
    def __p_enunciado(self):
        "Enunciado := ID"
        self.enunciado = None
        token = self.analex.preanalisis()
        self._emparejar(token, Token.ID)
        simbolo = token.valor
        enunciado = simbolo.valor
        if not enunciado:
            enunciado = Enunciado(simbolo.nombre)
            self.elementos[enunciado.id] = enunciado
        self.enunciado = enunciado
    
    def __p_conprop(self):
        "ConProp := Conectivo PropInterna | LAMBDA"
        self.conprop = None
        prop1 = self.propinterna
        token = self.analex.preanalisis()
        if token.tipo in self.F['pConectivo']:
            self.__p_conectivo()
            self.__p_propinterna()
            conprop = None
            if self.conectivo == Token.O:
                conprop = Disyuncion(prop1, self.propinterna)
            elif self.conectivo == Token.Y:
                conprop = Conjuncion(prop1, self.propinterna)
            elif self.conectivo == Token.SI:
                conprop = Implicacion(prop1, self.propinterna)
            elif self.conectivo == Token.SII:
                conprop = DobleImplicacion(prop1, self.propinterna)
            self.conprop = conprop
        else:
            #LAMBDA
            pass
    
    def __p_conectivo(self):
        "Conectivo := O | Y | SI | SII"
        self.conectivo = None
        token = self.analex.preanalisis()
        if token.tipo == Token.O:
            self._emparejar(token, Token.O)
            self.conectivo = Token.O
        elif token.tipo == Token.Y:
            self._emparejar(token, Token.Y)
            self.conectivo = Token.Y
        elif token.tipo == Token.SI:
            self._emparejar(token, Token.SI)
            self.conectivo = Token.SI
        elif token.tipo == Token.SII:
            self._emparejar(token, Token.SII)
            self.conectivo = Token.SII
        else:
            self._arrojar_error(self.F['pConectivo'])
    
    def __p_justificacion(self):
        "Justificacion := ReglaInferencia Parametros"
        self.justificacion = None
        self.__p_reglainferencia()
        self.__p_parametros()
        justificacion = Justificacion(self.regla_inferencia, self.parametros)
        self.justificacion = justificacion
    
    def __p_reglainferencia(self):
        "ReglaInferencia := MP | MT | MTP | SIMPL | ADJ | SH | SD | RP | DEM | \
            PDEM | DCOND | RAA | CONTR | EquivalenciaLogica"
        self.regla_inferencia = None
        token = self.analex.preanalisis()
        if token.tipo == Token.MP:
            self._emparejar(token, Token.MP)
            self.regla_inferencia = ModusPonens()
        elif token.tipo == Token.MT:
            self._emparejar(token, Token.MT)
            self.regla_inferencia = ModusTollens()
        elif token.tipo == Token.MTP:
            self._emparejar(token, Token.MTP)
            self.regla_inferencia = ModusTollendoPonens()
        elif token.tipo == Token.SIMPL:
            self._emparejar(token, Token.SIMPL)
            self.regla_inferencia = Simplificacion()
        elif token.tipo == Token.ADJ:
            self._emparejar(token, Token.ADJ)
            self.regla_inferencia = Adjuncion()
        elif token.tipo == Token.SH:
            self._emparejar(token, Token.SH)
            self.regla_inferencia = SilogismoHipotetico()
        elif token.tipo == Token.SD:
            self._emparejar(token, Token.SD)
            self.regla_inferencia = SilogismoDisyuntivo()
        elif token.tipo == Token.RP:
            self._emparejar(token, Token.RP)
            self.regla_inferencia = ReglaPremisas()
        elif token.tipo == Token.DEM:
            self._emparejar(token, Token.DEM)
            self.regla_inferencia = Demostrostrado()
        elif token.tipo == Token.PDEM:
            self._emparejar(token, Token.PDEM)
            self.regla_inferencia = PorDemostrar()
        elif token.tipo == Token.DCOND:
            self._emparejar(token, Token.DCOND)
            self.regla_inferencia = DemostracionCondicional()
        elif token.tipo == Token.RAA:
            self._emparejar(token, Token.RAA)
            self.regla_inferencia = ReduccionAlAbsurdo()
        elif token.tipo == Token.CONTR:
            self._emparejar(token, Token.CONTR)
            self.regla_inferencia = Contradiccion()
        elif token.tipo in self.F['pEquivalenciaLogica']:
            self.__p_equivalencialogica()
            self.regla_inferencia = self.equivalencia_logica
        else:
            self._arrojar_error(self.F['pReglaInferencia'])
    
    def __p_equivalencialogica(self):
        "EquivalenciaLogica := IDEMP | CONM | ASOC | DIST | IMPL | DIMPL | LDM \
            | TAUT | ATAUT | ABS | DBLNEG"
        self.equivalencia_logica = None
        token = self.analex.preanalisis()
        if token.tipo == Token.IDEMP:
            self._emparejar(token, Token.IDEMP)
            self.equivalencia_logica = Idempotencia()
        elif token.tipo == Token.CONM:
            self._emparejar(token, Token.CONM)
            self.equivalencia_logica = Conmutatividad()
        elif token.tipo == Token.ASOC:
            self._emparejar(token, Token.ASOC)
            self.equivalencia_logica = Asociatividad()
        elif token.tipo == Token.DIST:
            self._emparejar(token, Token.DIST)
            self.equivalencia_logica = Distributividad()
        elif token.tipo == Token.IMPL:
            self._emparejar(token, Token.IMPL)
            self.equivalencia_logica = Implicacion()
        elif token.tipo == Token.DIMPL:
            self._emparejar(token, Token.DIMPL)
            self.equivalencia_logica = DobleImplicacion()
        elif token.tipo == Token.LDM:
            self._emparejar(token, Token.LDM)
            self.equivalencia_logica = LeyDeMorgan()
        elif token.tipo == Token.TAUT:
            self._emparejar(token, Token.TAUT)
            self.equivalencia_logica = CondicionTautologia()
        elif token.tipo == Token.ATAUT:
            self._emparejar(token, Token.ATAUT)
            self.equivalencia_logica = CondicionAntitautologia()
        elif token.tipo == Token.ABS:
            self._emparejar(token, Token.ABS)
            self.equivalencia_logica = Absorcion()
        elif token.tipo == Token.DBLNEG:
            self._emparejar(token, Token.DBLNEG)
            self.equivalencia_logica = DobleNegacion()
        else:
            self._arrojar_error(self.F['pEquivalenciaLogica'])
    
    def __p_parametros(self):
        "Parametros := PABRE NUMERO MasNumero PCIERRA | LAMBDA"
        self.parametros = []
        token = self.analex.preanalisis()
        if token.tipo == Token.PABRE:
            self._emparejar(token, Token.PABRE)
            token = self.analex.preanalisis()
            self._emparejar(token, Token.NUMERO)
            self.parametros.append(str(token.valor))
            self.__p_masnumero()
            token = self.analex.preanalisis()
            self._emparejar(token, Token.PCIERRA)
        else:
            # LAMBDA
            pass
    
    def __p_masnumero(self):
        "MasNumero := COMA NUMERO MasNumero | LAMBDA"
        token = self.analex.preanalisis()
        if token.tipo == Token.COMA:
            self._emparejar(token, Token.COMA)
            token = self.analex.preanalisis()
            self._emparejar(token, Token.NUMERO)
            self.parametros.append(str(token.valor))
            self.__p_masnumero()
        else:
            # LAMBDA
            pass
    
    def __p_massentencia(self):
        "MasSentencia := Sentencia MasSentencia | LAMBDA"
        token = self.analex.preanalisis()
        if token.tipo in self.F['pSentencia']:
            self.__p_sentencia()
            self.__p_massentencia()
        else:
            # LAMBDA
            pass
